\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Qa}$, ${\it Rb}$, ${\it Sc}$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$, $C$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$),\+
\\[0ex]${\it Ic}$:AbsInterface($C$), $f_{1}$:(E(${\it Ia}$)$\rightarrow$$B$), $f_{2}$:($B$$\rightarrow$$C$), $g_{1}$:(E(${\it Ib}$)$\rightarrow$E), $g_{2}$:(E(${\it Ic}$)$\rightarrow$E).
\-\\[0ex]($g_{1}$ glues ${\it Ia}$:${\it Qa}$ $--$$f_{1}$$\rightarrow$ ${\it Ib}$:${\it Rb}$ \& $g_{2}$ glues ${\it Ib}$:${\it Rb}$ $--\lambda$$e$.$f_{2}$(${\it Ib}$($e$))$\rightarrow$ ${\it Ic}$:${\it Sc}$)
\\[0ex]$\Rightarrow$ $g_{1}$ o $g_{2}$ glues ${\it Ia}$:${\it Qa}$ $--$$f_{2}$ o $f_{1}$$\rightarrow$ ${\it Ic}$:${\it Sc}$
\end{tabbing}